$M$.X $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{$x$:Id$\mid$ fpf{-}dom(IdDeq; $x$; 1of($M$)) \}